$\forall$$A$:Type, $n$, $m$:$\mathbb{N}$, $f$:($A$$\rightarrow$($A$ + Top)), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply($f$\^{}$n$+$m$;$x$)) $\Leftarrow\!\Rightarrow$ (($\uparrow$can{-}apply($f$\^{}$m$;$x$)) \& ($\uparrow$can{-}apply($f$\^{}$n$;do{-}apply($f$\^{}$m$;$x$))))